$\forall$$A$, $B$:Type, $a$:EqDecider($A$), $b$:EqDecider($B$), $p$, $q$:($A$$\times$$B$). $p$ $=$ $q$ $\Leftrightarrow$ proddeq($a$;$b$)($p$,$q$)